Termination w.r.t. Q proof of TRS/secret06addList.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ADDLISTS₃(xs, ys, zs) -> ISZERO₁(head₁(xs))
ADDLIST₂(xs, ys) -> ADDLISTS₃(xs, ys, nil)
IF₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> ADDLISTS₃(xs, ys, zs2)
ADDLISTS₃(xs, ys, zs) -> IF₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
ADDLISTS₃(xs, ys, zs) -> INC₁(head₁(ys))
ADDLISTS₃(xs, ys, zs) -> ISEMPTY₁(ys)
ADDLISTS₃(xs, ys, zs) -> HEAD₁(ys)
ADDLISTS₃(xs, ys, zs) -> HEAD₁(xs)
ADDLISTS₃(xs, ys, zs) -> TAIL₁(ys)
ADDLISTS₃(xs, ys, zs) -> APPEND₂(zs, head₁(ys))
P₁(s₁(s₁(x))) -> P₁(s₁(x))
ADDLISTS₃(xs, ys, zs) -> TAIL₁(xs)
IF₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> ADDLISTS₃(xs2, ys2, zs)
ADDLISTS₃(xs, ys, zs) -> ISEMPTY₁(xs)
APPEND₂(cons₂(y, ys), x) -> APPEND₂(ys, x)
INC₁(s₁(x)) -> INC₁(x)
ADDLISTS₃(xs, ys, zs) -> P₁(head₁(xs))

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ADDLISTS₃(xs, ys, zs) -> ISZERO₁(head₁(xs))
ADDLIST₂(xs, ys) -> ADDLISTS₃(xs, ys, nil)
IF₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> ADDLISTS₃(xs, ys, zs2)
ADDLISTS₃(xs, ys, zs) -> IF₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
ADDLISTS₃(xs, ys, zs) -> INC₁(head₁(ys))
ADDLISTS₃(xs, ys, zs) -> ISEMPTY₁(ys)
ADDLISTS₃(xs, ys, zs) -> HEAD₁(ys)
ADDLISTS₃(xs, ys, zs) -> HEAD₁(xs)
ADDLISTS₃(xs, ys, zs) -> TAIL₁(ys)
ADDLISTS₃(xs, ys, zs) -> APPEND₂(zs, head₁(ys))
P₁(s₁(s₁(x))) -> P₁(s₁(x))
ADDLISTS₃(xs, ys, zs) -> TAIL₁(xs)
IF₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> ADDLISTS₃(xs2, ys2, zs)
ADDLISTS₃(xs, ys, zs) -> ISEMPTY₁(xs)
APPEND₂(cons₂(y, ys), x) -> APPEND₂(ys, x)
INC₁(s₁(x)) -> INC₁(x)
ADDLISTS₃(xs, ys, zs) -> P₁(head₁(xs))

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 4 SCCs with 11 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

INC₁(s₁(x)) -> INC₁(x)

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

INC₁(s₁(x)) -> INC₁(x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(INC₁(x₁)) = 3·x₁
POL(s₁(x₁)) = 1 + x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

P₁(s₁(s₁(x))) -> P₁(s₁(x))

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

P₁(s₁(s₁(x))) -> P₁(s₁(x))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(P₁(x₁)) = x₁
POL(s₁(x₁)) = 1 + 3·x₁

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND₂(cons₂(y, ys), x) -> APPEND₂(ys, x)

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

APPEND₂(cons₂(y, ys), x) -> APPEND₂(ys, x)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [21]:

POL(APPEND₂(x₁, x₂)) = 3·x₁
POL(cons₂(x₁, x₂)) = 1 + x₂

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> ADDLISTS₃(xs, ys, zs2)
IF₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> ADDLISTS₃(xs2, ys2, zs)
ADDLISTS₃(xs, ys, zs) -> IF₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))

The TRS R consists of the following rules:

isEmpty₁(cons₂(x, xs)) -> false
isEmpty₁(nil) -> true
isZero₁(0) -> true
isZero₁(s₁(x)) -> false
head₁(cons₂(x, xs)) -> x
tail₁(cons₂(x, xs)) -> xs
tail₁(nil) -> nil
append₂(nil, x) -> cons₂(x, nil)
append₂(cons₂(y, ys), x) -> cons₂(y, append₂(ys, x))
p₁(s₁(s₁(x))) -> s₁(p₁(s₁(x)))
p₁(s₁(0)) -> 0
p₁(0) -> 0
inc₁(s₁(x)) -> s₁(inc₁(x))
inc₁(0) -> s₁(0)
addLists₃(xs, ys, zs) -> if₉(isEmpty₁(xs), isEmpty₁(ys), isZero₁(head₁(xs)), tail₁(xs), tail₁(ys), cons₂(p₁(head₁(xs)), tail₁(xs)), cons₂(inc₁(head₁(ys)), tail₁(ys)), zs, append₂(zs, head₁(ys)))
if₉(true, true, b, xs, ys, xs2, ys2, zs, zs2) -> zs
if₉(true, false, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, true, b, xs, ys, xs2, ys2, zs, zs2) -> differentLengthError
if₉(false, false, false, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs2, ys2, zs)
if₉(false, false, true, xs, ys, xs2, ys2, zs, zs2) -> addLists₃(xs, ys, zs2)
addList₂(xs, ys) -> addLists₃(xs, ys, nil)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.